grammar DQC;

options {
  language = Java;
}

@header {
package parsing;

import util.*;
import ast.*;
import ast.Process;
import java.util.ArrayList;
}

@lexer::header {
package parsing;
}

system returns [DQCSystem value]
    : 'define' {ArrayList<Procedure> lst = new ArrayList<Procedure>();} (pd = procedure_def {lst.add(pd);})* 'in' n = parallel_network 'using' '(' il = idtp_list ')' ',' '(' id_list ')' 
      'with_ph' afl = af_list {ArrayList<Function> fl = new ArrayList<Function>();}
	  ('with_fun' fsd=fun_sig_def {fl.add(fsd);}
	  		(';' fsd=fun_sig_def {fl.add(fsd);})*
	  )? {$value = new DQCSystem(lst, n, il, afl, fl);}
	  EOF 
    ;
	
fun_sig_def returns [Function value]
	: ID ':' s=srt 
		  {ArrayList<String> sl = new ArrayList<String>();
		   sl.add(s);} 
		  (',' s=srt {sl.add(s);})* '->' s2=srt 
		  {Pair<ArrayList<String>,String> p1 = new Pair<ArrayList<String>,String>(sl, s2);} 
		  'is' d=def {$value = new Function($ID.getText(), p1, d);}
	;

def returns [ArrayList<Pair<ArrayList<String>, String>> value]
	: il=id_list '->' id1=ID 
	{$value = new ArrayList<Pair<ArrayList<String>, String>>();
	 $value.add(new Pair(il, id1.getText()));}
	(',' il2=id_list '->' id2=ID {$value.add(new Pair(il2,id2.getText()));})*
	;

srt returns [String value]
	: 'Ch' {$value = "Ch";}
	| 'Dt' {$value = "Dt";}
	| 'Pr' {$value = "Pr";}
	| 'St' {$value = "St";}
	;

af_list returns [ArrayList<Pair<String,String>> value]
: {$value = new ArrayList<Pair<String,String>>();}
| id1 = ID '>' id2 = ID 
	{$value = new ArrayList<Pair<String,String>>();
	 $value.add(new Pair<String,String>(id1.getText(), id2.getText()));}
(',' id3 = ID '>' id4 = ID {$value.add(new Pair<String,String>(id3.getText(), id4.getText()));})*
	;

idtp_list returns [ArrayList<Constant> value]
:   {$value = new ArrayList<Constant>();}
|   {$value = new ArrayList<Constant>();}
	id1 = ID ':' t=tp 
	{
		if (t instanceof Data) {
			$value.add(new DataConstant(id1.getText()));
		} else {
			$value.add(new ChannelConstant(id1.getText(), t));
		}
	}
	(',' id2 = ID ':' t=tp 
	{
		if (t instanceof Data) {
			$value.add(new DataConstant(id2.getText()));
		} else {
			$value.add(new ChannelConstant(id2.getText(), t));
		}
	}
	)*
;

procedure_def returns [Procedure value]
    : id1 = ID cl=comp_label '@' id2 = ID '(' il = id_list ')' 'as' p = parallel_process 
	  {$value = new Procedure(id1.getText(), new Site(id2.getText()), il, p, cl);}
    ;
	
parallel_network returns [Network value]
	: n = network {ArrayList<Network> lst = new ArrayList<Network>(); lst.add(n);}
	 ('|' n = network {lst.add(n);})* {$value = new ParallelNetwork(lst);}
	;
	 
network returns [Network value]
    : '(' '@' ID ')' '(' p = parallel_process {$value = new ProcessAtSite(new Site($ID.getText()), p); } ')'
	| '(' 'new' ID ':' t = tp ')' '(' n = parallel_network ')'
	  {
	  	if (t instanceof Data) {
	  		$value = new NewConstN(new DataConstant($ID.getText()), n);
	  	} else {
	  		$value = new NewConstN(new ChannelConstant($ID.getText(), t), n);
	  	}
	  }
	;
	
comp_label returns [Label value]
	: lc = label_conjunction {ArrayList<Label> lst = new ArrayList<Label>(); lst.add(lc);} ('+' lc = label_conjunction {lst.add(lc);})* {$value = new LabelDisjunction(lst);}
	;
	
label_conjunction returns [Label value]
	: l = label {ArrayList<Label> lst = new ArrayList<Label>(); lst.add(l);} 
		('*' l = label {lst.add(l);})* {$value = new LabelConjunction(lst);}
	;
	
label returns [Label value]
    : '{' t=term '<-' il = trm_list '}' {$value = new AtomicLabel(t, il);}
    | '(' cl = comp_label ')' {$value = cl;}
    ;

parallel_process returns [ParallelProcess value]
    : p = process {ArrayList<Process> lst = new ArrayList<Process>(); lst.add(p);}  ('|' p = process {lst.add(p);} )* {$value = new ParallelProcess(lst);}
    ;
    
process returns [Process value]
    : '0' {$value = new Zero();}
    | '(' 'new' ID ':' typ=tp ')' '(' p=parallel_process ')'
	  { 
	  	if (typ instanceof Data) {
			$value = new NewConstP(new DataConstant($ID.getText()), p);
		} else {
			$value = new NewConstP(new ChannelConstant($ID.getText(), typ), p);
		}
	  }
    | 'go' '(' t = term ')' '.' p = parallel_process {$value = new Go(t, p);}
    | 'dummy' '(' p = parallel_process ')' {$value = new Dummy(p);}
    | b = binder '.' p = parallel_process {$value = new PrefixedProcess(b, p);}
    | 'case' e = exp 'of' 'some' '(' ID ')' ':' p1 = parallel_process 'else' p2 = parallel_process 
	  {$value = new Case(e, new TermVar($ID.getText()), p1, p2);}
    | 'acts_for' '(' t1 = term ',' t2 = term')' ':' p1 = parallel_process 'else' p2=parallel_process
	  {$value = new ActsFor(t1, t2, p1, p2);}
    | ID '(' el = exp_list ')' {$value = new Call($ID.getText(), el);}
    | '(' p=parallel_process ')' {$value = p;}
    ;		
    
tp returns [Type value]
	: 'Dt' {$value = new Data();}
	| 'ext' l = comp_label {l.setExternal(true); $value = l;}
	| 'int' l = comp_label {l.setExternal(false); $value = l;}
	;

binder returns [Binder value]
	: t = term ( '!' t1 = term {$value = new Out(t, t1);} 
	                | '?' ID {$value = new In(t, new ExpVar($ID.getText()));} )
	| '&' '_' q = quality_pred '(' bl = binder_list ')' 
		{$value = new CompositeBinder(q, bl);}
	| 'assert' '(' l1 = comp_label ',' l2 = comp_label ',' b = binder ')'
	{$value = new Assert(b, l1, l2);}
	;
	
quality_pred returns [QualityPredicate value]
	: 'a' {$value = new ForallPredicate();}
	| 'e' {$value = new ExistsPredicate();}
	| bf = boolean_formula {$value = bf;}
	;

boolean_formula returns [QualityPredicate value]
	: af = and_formula 
	  {ArrayList<QualityPredicate> lst = new ArrayList<QualityPredicate>(); lst.add(af);} 
	  ('||' af = and_formula {lst.add(af);})* {$value = new OrPredicate(lst);}
	;

and_formula returns [AndPredicate value]
	: af = atom_formula  
	  {ArrayList<QualityPredicate> lst = new ArrayList<QualityPredicate>(); lst.add(af);}
	('&&' af=atom_formula {lst.add(af);})* {$value = new AndPredicate(lst);}
	;

atom_formula returns [QualityPredicate value]
	: NUM {$value = new NumPredicate(Integer.parseInt($NUM.getText()));}
	| '(' bf = boolean_formula ')' {$value = bf;}
	;

binder_list returns [ArrayList<Binder> value]
 	: b = binder {$value = new ArrayList<Binder>(); $value.add(b);} (',' b = binder {$value.add(b);})*
	;
	
exp returns [Expression value]
	: 'some' '(' t = term ')' {$value = new Some(t);}
	| 'none' {$value = new None();}
	| ID {$value = new ExpVar($ID.getText());}
	;
	
term returns [Term value]
	: ID {$value = new TermVar($ID.getText());}
	| ID '(' tl = trm_list ')' {$value = new FunApp($ID.getText(), tl);}
	| 'endorse' '(' l1 = comp_label ',' l2 = comp_label ',' t = term ')' 
	  {$value = new Endorse(t, l1, l2);}
	| '*' {$value = new TermVar("*");}
	| '_' {$value = new TermVar("_");}
	;

trm_list returns [ArrayList<Term> value]
	: {$value = new ArrayList<Term>();}
	| t = term {$value = new ArrayList<Term>(); $value.add(t);} (',' t=term {$value.add(t);})*
	;
	
exp_list returns [ArrayList<Expression> value]
	: {$value = new ArrayList<Expression>();}
	| e = exp {$value = new ArrayList<Expression>(); $value.add(e);} (',' e=exp
	  {$value.add(e);} )*
	;
	
id_list returns [ArrayList<String> value]
	: {$value = new ArrayList<String>(); }
	| id1 = ID {$value = new ArrayList<String>(); $value.add(id1.getText());} 
	  (',' id2 = ID {$value.add(id2.getText());})*
	;
    
NUM : ('0'..'9')+ ;
ID  : ('a'..'z'|'A'..'Z')('a'..'z'|'A'..'Z'|'0'..'9')* ;
WS  :   (' '|'\t'|'\r'|'\n')+ { $channel = HIDDEN; } ; 
